A:Type, I:MaInterface(A), es:ES, v:Id.
ma-interface-consistent2(es;I)
 (v  ma-interface-locs(I))
 (e:E. ((e  [[I|v]]))  ((e  [[I]]))) 

latex

Definitions

P  Q, x:A. B(x), ma-interface-consistent(es;X), [[I|i]], t  T, e  X, b, E, Id, (x  l), ma-interface-consistent2(es;I), ES, MaInterface(T), Type, False, A, left + right, P  Q, Dec(P), Knd, ma-interface-dom(I;i), kind(e), b, s = t, , , x:AB(x), x:A  B(x), P & Q, P  Q, Unit, can-apply(f;x), [[X]], ma-interface-locs(I), {T}, SQType(T), s ~ t, Atom$n, ma-interface-info(I;i;k), ma-interface-code(I;i;k), ma-interface-val(es;X;e), a:A fp B(a), e@i. P(e), a < b, t.1, if b then t else f fi , type List, Void, x:A.B(x), Top, State(ds), {x:A| B(x)} , x:A. B(x), let x,y = A in B(x;y), case b of inl(x) => s(x) | inr(y) => t(y), <a, b>, hasloc(k;i), S  T, x. t(x), x.A(x), IdLnk, fpf-domain(f), #$n, ||as||, A  B, , , l[i], A c B, P  Q, f(x), KindDeq

Lemmas

assert-ma-in-interface, Id wf, member-fpf-dom, Knd wf, Kind-deq wf, fpf-ap wf, member-fpf-domain, length wf nat, nat wf, select wf, IdLnk wf, fpf-domain wf, fpf-trivial-subtype-top, subtype rel product, subtype rel list, subtype rel function, decl-state wf, top wf, subtype rel set, l member wf, hasloc wf, subtype-set-hasloc, Id sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, ma-interface-triggers-loc, decidable l member, decidable equal Kind, ma-interface-triggers-kind, assert wf, es-is-interface wf, ma-interface-triggers wf, ma-interface-consistent-consistent2, ma-interface-triggers-can-apply